This invention relates to program analysis techniques, and in particular generating hints for use in program analysis, for example, a program which relates to an integrated circuit design.
The design of integrated circuit devices conventionally uses hardware description languages (HDLs) to describe circuits (herein also sometimes called “systems”) at various levels of abstraction. As a circuit design evolves, designers and verification engineers (whose job it is to assure that the design functions appropriately) conduct analysis of the device being designed to evaluate the quality of the design and to hopefully find and eliminate any inadequacies potentially leading to future problems such as impossibility or inaccuracy in performance of the device.
One problem encountered in such analysis is referred to as a “state explosion”, which occurs when an input to the design, intended to permit analysis of the response of the device to a particular input, generates such a large number of possible output or intermediate states as to overrun any memory used in supporting the analysis.
Reach-ability analysis plays a central role in formal verification of sequential circuits. One of the state-of-the-art approaches for reach-ability analysis and formal verification of circuits modeled as Finite State Machines (FSMs) exploits symbolic computations based on Binary Decision Diagrams (BDDs). However, the known state explosion problem may cause large intermediate BDD sizes during the exploration of the state space of a system. The conventional breadth-first search (BFS) strategy, used in most implicit model checking algorithms, is the main culprit. Others have approached this problem by devising techniques that simplify the system model employed during BFS.
Some recent work in avoiding the state explosion problem during one known analysis procedure, breadth-first symbolic traversal based on Binary Decision Diagrams (BDDs), applies hints to constrain the transition relation of the system to be verified. Hints are expressed as constraints on the primary inputs and states of a circuit modeled as a Finite State Machine (FSM) and can often be found with the help of simple heuristics by someone who understands the circuit well enough to devise simulation stimuli or verification properties for it. However, the ease of finding good hints is limited by the size and complexity of the design, and extending their applicability to larger designs is a key issue.
In one such proposal, “hints” are used to guide the exploration of the state space. In that proposal, hints are classified into those that depend on the invariants being checked (proving properties that should hold in all reachable states of a system) and those that capture knowledge of the design. Hints are applied by constraining the transition relation of the system; the constrained traversal of the state space proceeds much faster than the unconstrained system (original transition relation). This method obtained orders-of-magnitude reductions in time and space requirements during the exploration of the state space. Hints can often be found by someone who understands the design well enough to devise simulation stimuli or verification properties for it. However, in large complex designs, identifying good hints can be a labor-intensive process requiring many attempts, and in most cases does not avoid the state space explosion problem. Acceptance of this method by designers and verification engineers will certainly benefit from a more efficient technique to devise good hints from a system being verified.
Accordingly, in co-pending application Ser. No. 10/966492 a method for generating hints for use in analyzing an original program was disclosed in which: first, the original program is partitioned into sub-programs representing valid computational paths; second, each subprogram is refined when cyclic dependencies are found to exist between the variables; third, computational paths whose over-approximated reachable states are found to be contained in another computational path are merged; and finally, the remaining subprograms conjoined decision conditions become candidates for hints.
In this method the step of partitioning the original program is an important step in controlling the number and quality of the candidate hints produced, and the problem of partitioning the original program is addressed by the present invention.